Skip to content

feat(LinearAlgebra/Basis/HasCanonicalBasis): propose HasCanonicalBasis class#39253

Draft
Paul-Lez wants to merge 5 commits into
leanprover-community:masterfrom
Paul-Lez:chosen-basis
Draft

feat(LinearAlgebra/Basis/HasCanonicalBasis): propose HasCanonicalBasis class#39253
Paul-Lez wants to merge 5 commits into
leanprover-community:masterfrom
Paul-Lez:chosen-basis

Conversation

@Paul-Lez
Copy link
Copy Markdown
Collaborator

@Paul-Lez Paul-Lez commented May 12, 2026

This PR continues the work from #25425.

Original PR: #25425

Paul-Lez and others added 4 commits June 4, 2025 10:50
@Paul-Lez Paul-Lez mentioned this pull request May 12, 2026
Closed
@github-actions
Copy link
Copy Markdown

github-actions Bot commented May 12, 2026

PR summary 7e31c21f9f

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.LinearAlgebra.Basis.HasCanonicalBasis (new file) 2152

Declarations diff

+ EuclideanSpace.hasCanonicalBasis
+ HasCanonicalBasis
+ Pi.hasCanonicalBasis
+ basis_apply
+ instance : HasCanonicalBasis 𝕜 (𝕜 × 𝕜 × 𝕜) (Fin 3)
+ instance : HasCanonicalBasis 𝕜 (𝕜 × 𝕜) (Fin 2) (![(1, 0), (0, 1)])
+ instance : HasCanonicalBasis 𝕜 𝕜 (Fin 1) (fun _ ↦ 1)
+ instance [Ring 𝕜] (p : ENNReal) :
+ prod
+ reindex

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.
No changes to weak technical debt.

@github-actions github-actions Bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 12, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@Paul-Lez